table → gen(s(0))
gen(x) → if1(le(x, 10), x)
if1(false, x) → nil
if1(true, x) → if2(x, x)
if2(x, y) → if3(le(y, 10), x, y)
if3(true, x, y) → cons(entry(x, y, times(x, y)), if2(x, s(y)))
if3(false, x, y) → gen(s(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
10 → s(s(s(s(s(s(s(s(s(s(0))))))))))
↳ QTRS
↳ DependencyPairsProof
table → gen(s(0))
gen(x) → if1(le(x, 10), x)
if1(false, x) → nil
if1(true, x) → if2(x, x)
if2(x, y) → if3(le(y, 10), x, y)
if3(true, x, y) → cons(entry(x, y, times(x, y)), if2(x, s(y)))
if3(false, x, y) → gen(s(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
10 → s(s(s(s(s(s(s(s(s(s(0))))))))))
IF3(false, x, y) → GEN(s(x))
IF2(x, y) → 101
IF2(x, y) → LE(y, 10)
GEN(x) → LE(x, 10)
IF3(true, x, y) → IF2(x, s(y))
GEN(x) → 101
LE(s(x), s(y)) → LE(x, y)
TIMES(s(x), y) → PLUS(y, times(x, y))
IF3(true, x, y) → TIMES(x, y)
TABLE → GEN(s(0))
TIMES(s(x), y) → TIMES(x, y)
GEN(x) → IF1(le(x, 10), x)
IF1(true, x) → IF2(x, x)
IF2(x, y) → IF3(le(y, 10), x, y)
PLUS(s(x), y) → PLUS(x, y)
table → gen(s(0))
gen(x) → if1(le(x, 10), x)
if1(false, x) → nil
if1(true, x) → if2(x, x)
if2(x, y) → if3(le(y, 10), x, y)
if3(true, x, y) → cons(entry(x, y, times(x, y)), if2(x, s(y)))
if3(false, x, y) → gen(s(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
10 → s(s(s(s(s(s(s(s(s(s(0))))))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
IF3(false, x, y) → GEN(s(x))
IF2(x, y) → 101
IF2(x, y) → LE(y, 10)
GEN(x) → LE(x, 10)
IF3(true, x, y) → IF2(x, s(y))
GEN(x) → 101
LE(s(x), s(y)) → LE(x, y)
TIMES(s(x), y) → PLUS(y, times(x, y))
IF3(true, x, y) → TIMES(x, y)
TABLE → GEN(s(0))
TIMES(s(x), y) → TIMES(x, y)
GEN(x) → IF1(le(x, 10), x)
IF1(true, x) → IF2(x, x)
IF2(x, y) → IF3(le(y, 10), x, y)
PLUS(s(x), y) → PLUS(x, y)
table → gen(s(0))
gen(x) → if1(le(x, 10), x)
if1(false, x) → nil
if1(true, x) → if2(x, x)
if2(x, y) → if3(le(y, 10), x, y)
if3(true, x, y) → cons(entry(x, y, times(x, y)), if2(x, s(y)))
if3(false, x, y) → gen(s(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
10 → s(s(s(s(s(s(s(s(s(s(0))))))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
↳ QDP
PLUS(s(x), y) → PLUS(x, y)
table → gen(s(0))
gen(x) → if1(le(x, 10), x)
if1(false, x) → nil
if1(true, x) → if2(x, x)
if2(x, y) → if3(le(y, 10), x, y)
if3(true, x, y) → cons(entry(x, y, times(x, y)), if2(x, s(y)))
if3(false, x, y) → gen(s(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
10 → s(s(s(s(s(s(s(s(s(s(0))))))))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PLUS(s(x), y) → PLUS(x, y)
The value of delta used in the strict ordering is 1/16.
POL(PLUS(x1, x2)) = (1/4)x_1
POL(s(x1)) = 1/4 + (2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
table → gen(s(0))
gen(x) → if1(le(x, 10), x)
if1(false, x) → nil
if1(true, x) → if2(x, x)
if2(x, y) → if3(le(y, 10), x, y)
if3(true, x, y) → cons(entry(x, y, times(x, y)), if2(x, s(y)))
if3(false, x, y) → gen(s(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
10 → s(s(s(s(s(s(s(s(s(s(0))))))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
TIMES(s(x), y) → TIMES(x, y)
table → gen(s(0))
gen(x) → if1(le(x, 10), x)
if1(false, x) → nil
if1(true, x) → if2(x, x)
if2(x, y) → if3(le(y, 10), x, y)
if3(true, x, y) → cons(entry(x, y, times(x, y)), if2(x, s(y)))
if3(false, x, y) → gen(s(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
10 → s(s(s(s(s(s(s(s(s(s(0))))))))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
TIMES(s(x), y) → TIMES(x, y)
The value of delta used in the strict ordering is 1/16.
POL(TIMES(x1, x2)) = (1/4)x_1
POL(s(x1)) = 1/4 + (2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
table → gen(s(0))
gen(x) → if1(le(x, 10), x)
if1(false, x) → nil
if1(true, x) → if2(x, x)
if2(x, y) → if3(le(y, 10), x, y)
if3(true, x, y) → cons(entry(x, y, times(x, y)), if2(x, s(y)))
if3(false, x, y) → gen(s(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
10 → s(s(s(s(s(s(s(s(s(s(0))))))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
LE(s(x), s(y)) → LE(x, y)
table → gen(s(0))
gen(x) → if1(le(x, 10), x)
if1(false, x) → nil
if1(true, x) → if2(x, x)
if2(x, y) → if3(le(y, 10), x, y)
if3(true, x, y) → cons(entry(x, y, times(x, y)), if2(x, s(y)))
if3(false, x, y) → gen(s(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
10 → s(s(s(s(s(s(s(s(s(s(0))))))))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
LE(s(x), s(y)) → LE(x, y)
The value of delta used in the strict ordering is 1.
POL(s(x1)) = 1 + x_1
POL(LE(x1, x2)) = x_2
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
table → gen(s(0))
gen(x) → if1(le(x, 10), x)
if1(false, x) → nil
if1(true, x) → if2(x, x)
if2(x, y) → if3(le(y, 10), x, y)
if3(true, x, y) → cons(entry(x, y, times(x, y)), if2(x, s(y)))
if3(false, x, y) → gen(s(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
10 → s(s(s(s(s(s(s(s(s(s(0))))))))))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
IF3(false, x, y) → GEN(s(x))
IF3(true, x, y) → IF2(x, s(y))
GEN(x) → IF1(le(x, 10), x)
IF1(true, x) → IF2(x, x)
IF2(x, y) → IF3(le(y, 10), x, y)
table → gen(s(0))
gen(x) → if1(le(x, 10), x)
if1(false, x) → nil
if1(true, x) → if2(x, x)
if2(x, y) → if3(le(y, 10), x, y)
if3(true, x, y) → cons(entry(x, y, times(x, y)), if2(x, s(y)))
if3(false, x, y) → gen(s(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
times(0, y) → 0
times(s(x), y) → plus(y, times(x, y))
10 → s(s(s(s(s(s(s(s(s(s(0))))))))))